i:Id, p:finite-prob-space, ds:fpf(Id; x.Type), P:(decl-state(ds)).
normal-ds{i:l}(ds)  es-real{i:l}(es.pre-p(es; i; ds; mkid{a:ut2}; p; P)) 

latex

Definitions	event_system{i:l}, t  T, x:A. B(x), pre-p(es; i; ds; a; p; P), Type, prop{i:l}, x.A(x), x. t(x), R-realizes{i:l}(R; es.P(es)), atom{$n:n}, Id, {x:A| B(x)} , finite-prob-space, x:A  B(x), fpf(A; a.B(a)), x:AB(x), b, fpf-all(A; eq; f; x,v.P(x;v)), normal-ds{i:l}(ds), P  Q, x:A. B(x), es-real{i:l}(es.P(es)), , decl-state(ds), mkid{$x:ut2}, Rpre(loc; ds; a; p; P)
Lemmas	normal-ds wf, decl-state wf, bool wf, fpf wf, finite-prob-space wf, Id wf, Rpre wf, R-pre-rule, R-realizes wf, pre-p wf, event system wf